$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{P}$), $B$:($A$$\rightarrow$Type). $a$:\{$a$:$A$$\mid$ $P$($a$)\} fp$\rightarrow$ $B$($a$) $\subseteq$r $a$:$A$ fp$\rightarrow$ $B$($a$)